Papers with math and logic reasoning tasks
Efficient PRM Training Data Synthesis via Formal Verification (2026.findings-acl)
Copied to clipboard
Ryo Kamoi, Yusen Zhang, Nan Zhang, Sarkar Snigdha Sarathi Das, Ranran Haoran Zhang, Wenpeng Yin, Rui Zhang
| Challenge: | Existing approaches for constructing PRM training data rely on human annotation or sampling-based labeling methods that require repeated LLM calls. |
| Approach: | They propose a framework that synthesizes PRM training data by annotating step-level error labels using formal verification tools such as Z3 and Isabelle. |
| Outcome: | The proposed framework synthesizes PRM training data from formal logic and theorem proving tasks without human annotation or additional LLM calls. |